Soundiness dialog for making assumptions explicit by mattulbrich · Pull Request #3887 · KeYProject/key

mattulbrich · 2026-07-03T20:40:20Z

This pull request is a new feature: A dialog to display the sound(i)ness assumptions of KeY explicitly.

Intended Change

Implements a soundiness info window (reachable via context menu on the proof list or a button in the proof statistics dialog) that analyzes KeY proofs and displays potential sources of unsoundness in a structured HTML report. The feature helps users identify taclet options, and proof characteristics, and dependencies that may affect verification soundness.

Key features:

General KeY Settings analysis (source consistency, JML activation)
Taclet Options analysis with plain English impact descriptions
section removed from dialog, not yet implemented: Source Analysis (skeleton for future expansion)
Proof Tree Analysis (goals, lemmas, assumptions, rule applications, dependency analysis)
Disclaimer about KeY limitations (reflection, native methods, sequentiality, floating-point)

Future tasks (move to future feature request for next KeY version):

Refactor to StringTemplate or similar
Implement source analysis (What exactly should this contain?)
Address some of the comments of Soundiness dialog for making assumptions explicit #3887 (comment), e.g. refer to supported Java/JML features, explain proof caching

Screenshot:

Type of pull request

New feature (non-breaking change which adds functionality)
Refactoring (behaviour should not change or only minimally change)
There are changes to the (Java) code

Ensuring quality

I made sure that introduced/changed code is well documented (javadoc and inline comments): More or less, and easy to understand
I have tested the feature as follows: Opened proof statistics dialog, clicked "Show Soundiness Report" button, verified HTML report displays correctly with all four compartments (General KeY Settings, Taclet Options, Source Analysis, Proof Tree Analysis).
I have checked that runtime performance has not deteriorated: The information is only collected when opening the dialog, which seems instant on the proofs I tested (a few thousand nodes).

Additional information and contact(s)

Files added/modified:

key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessAnalyzer.java - Static utility class generating HTML reports
key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessDialog.java - Simple modal dialog displaying HTML
key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/SoundinessExtension.java - Extension point registration
key.ui/src/main/java/de/uka/ilkd/key/gui/soundiness/ShowSoundinessAction.java - Context menu action
key.ui/src/main/java/de/uka/ilkd/key/gui/windows/ShowProofStatistics.java - Added soundiness button

Documentation updated:

to delete: AGENT.soundiness.md - Design document
to delete: IMPLEMENTATION_SUMMARY.md - Implementation summary

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

by Qwen3.5 397B A17B, authored and extended by @WolframPfeifer

by Qwen3.5 397B A17B

unp1 · 2026-07-04T18:14:01Z

Thanks! Like it :-) Only bikesheding: For stricter then necessary, orange seems more like a warning. Dark green or blue?

WolframPfeifer · 2026-07-09T14:41:00Z

List of things that came to my mind while playing around a bit with the prototype:

The taclet options list should also show the key, not only the value (i.e. "runtimeExceptions:ban" instead of "ban" at the moment).
I think the description "arithmetic wraps around like in Java" for arithmeticSemanticsIgnoringOF is wrong
Should the dialog also explain about proof caching? Due to the pragmatics of the implementation, we are only absolutely sure that a cache hit is applicable (i.e., replayable at the current proof) after doing the replay. There might be "spurious" cache hits, even if I am not sure where they come from.
The proof statistics dialog looks weirdly wide now due to the new button.
I would prefer a bullet point list also for "1. General KeY Soundness", to make it easier to read.
http://soundiness.org/ lists the following things (among what is already shown in the dialog). Not sure what we should mention explicitly:
- implicit method invocations (finalizers, class initializers, Thread.<init>, etc.)
- exceptions and flow related to that
- invokedynamic
- code generation at runtime, dynamic loading
- different class loaders
- key native methods (Object.run, Object.doPrivileged)
The dialog might also be a good place to list some information from https://www.key-project.org/applications/program-verification/ (generics, library methods, ...) or even https://www.key-project.org/jml-support-in-key/ (maybe semantics of assignable/accessible, invariants?), or link to these pages.
What about dependencies to other contracts? The information is present (I think in class ProofCorrectnessMgt) and shown in the proof list, but maybe it should also be listed here.

…sis stub

WolframPfeifer · 2026-07-13T15:55:53Z

Thanks! Like it :-) Only bikesheding: For stricter then necessary, orange seems more like a warning. Dark green or blue?

I changed the color to blue now.

WolframPfeifer · 2026-07-13T16:56:14Z

Just fixed one more thing: The calculation of goals/steps was wrong (showed steps but labelled it as goals, and did not correctly calculate the automatic/interactive steps). Now, the implementation is fixed by using the existing proof statistics.

soundiness first steps

14f9c21

by Qwen3.5 397B A17B

mattulbrich added this to the v3.0.0 milestone Jul 3, 2026

mattulbrich self-assigned this Jul 3, 2026

mattulbrich marked this pull request as draft July 3, 2026 20:40